Proof of Theorem fpwwe2lem5
Step | Hyp | Ref
| Expression |
1 | | fpwwe2.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝐴 ∈ V) |
3 | | simpr1 1067 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑋 ⊆ 𝐴) |
4 | 2, 3 | ssexd 4805 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑋 ∈ V) |
5 | | xpexg 6960 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V) |
6 | 4, 4, 5 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋 × 𝑋) ∈ V) |
7 | | simpr2 1068 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑅 ⊆ (𝑋 × 𝑋)) |
8 | 6, 7 | ssexd 4805 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑅 ∈ V) |
9 | 4, 8 | jca 554 |
. 2
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋 ∈ V ∧ 𝑅 ∈ V)) |
10 | | sseq1 3626 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴)) |
11 | | xpeq12 5134 |
. . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑥 = 𝑋) → (𝑥 × 𝑥) = (𝑋 × 𝑋)) |
12 | 11 | anidms 677 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 × 𝑥) = (𝑋 × 𝑋)) |
13 | 12 | sseq2d 3633 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑋 × 𝑋))) |
14 | | weeq2 5103 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑋)) |
15 | 10, 13, 14 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋))) |
16 | 15 | anbi2d 740 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) ↔ (𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)))) |
17 | | oveq1 6657 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥𝐹𝑟) = (𝑋𝐹𝑟)) |
18 | 17 | eleq1d 2686 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑥𝐹𝑟) ∈ 𝐴 ↔ (𝑋𝐹𝑟) ∈ 𝐴)) |
19 | 16, 18 | imbi12d 334 |
. . 3
⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)) → (𝑋𝐹𝑟) ∈ 𝐴))) |
20 | | sseq1 3626 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑟 ⊆ (𝑋 × 𝑋) ↔ 𝑅 ⊆ (𝑋 × 𝑋))) |
21 | | weeq1 5102 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑟 We 𝑋 ↔ 𝑅 We 𝑋)) |
22 | 20, 21 | 3anbi23d 1402 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋) ↔ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋))) |
23 | 22 | anbi2d 740 |
. . . 4
⊢ (𝑟 = 𝑅 → ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)) ↔ (𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)))) |
24 | | oveq2 6658 |
. . . . 5
⊢ (𝑟 = 𝑅 → (𝑋𝐹𝑟) = (𝑋𝐹𝑅)) |
25 | 24 | eleq1d 2686 |
. . . 4
⊢ (𝑟 = 𝑅 → ((𝑋𝐹𝑟) ∈ 𝐴 ↔ (𝑋𝐹𝑅) ∈ 𝐴)) |
26 | 23, 25 | imbi12d 334 |
. . 3
⊢ (𝑟 = 𝑅 → (((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)) → (𝑋𝐹𝑟) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴))) |
27 | | fpwwe2.3 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
28 | 19, 26, 27 | vtocl2g 3270 |
. 2
⊢ ((𝑋 ∈ V ∧ 𝑅 ∈ V) → ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴)) |
29 | 9, 28 | mpcom 38 |
1
⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴) |