Step | Hyp | Ref
| Expression |
1 | | mreexexlemd.6 |
. 2
⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾)) |
2 | | mreexexlemd.4 |
. 2
⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) |
3 | | mreexexlemd.5 |
. 2
⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) |
4 | | mreexexlemd.7 |
. . . 4
⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼))) |
5 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑢 = 𝑓) |
6 | 5 | breq1d 4593 |
. . . . . . . . . 10
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ≈ 𝐾 ↔ 𝑓 ≈ 𝐾)) |
7 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑣 = 𝑔) |
8 | 7 | breq1d 4593 |
. . . . . . . . . 10
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣 ≈ 𝐾 ↔ 𝑔 ≈ 𝐾)) |
9 | 6, 8 | orbi12d 742 |
. . . . . . . . 9
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ↔ (𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾))) |
10 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑡 = ℎ) |
11 | 7, 10 | uneq12d 3730 |
. . . . . . . . . . 11
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣 ∪ 𝑡) = (𝑔 ∪ ℎ)) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑁‘(𝑣 ∪ 𝑡)) = (𝑁‘(𝑔 ∪ ℎ))) |
13 | 5, 12 | sseq12d 3597 |
. . . . . . . . 9
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ↔ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))) |
14 | 5, 10 | uneq12d 3730 |
. . . . . . . . . 10
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ∪ 𝑡) = (𝑓 ∪ ℎ)) |
15 | 14 | eleq1d 2672 |
. . . . . . . . 9
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢 ∪ 𝑡) ∈ 𝐼 ↔ (𝑓 ∪ ℎ) ∈ 𝐼)) |
16 | 9, 13, 15 | 3anbi123d 1391 |
. . . . . . . 8
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) ↔ ((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼))) |
17 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑢 = 𝑓) |
18 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗) |
19 | 17, 18 | breq12d 4596 |
. . . . . . . . . 10
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑢 ≈ 𝑖 ↔ 𝑓 ≈ 𝑗)) |
20 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑡 = ℎ) |
21 | 18, 20 | uneq12d 3730 |
. . . . . . . . . . 11
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑖 ∪ 𝑡) = (𝑗 ∪ ℎ)) |
22 | 21 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑖 ∪ 𝑡) ∈ 𝐼 ↔ (𝑗 ∪ ℎ) ∈ 𝐼)) |
23 | 19, 22 | anbi12d 743 |
. . . . . . . . 9
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼) ↔ (𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼))) |
24 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑣 = 𝑔) |
25 | 24 | pweqd 4113 |
. . . . . . . . 9
⊢ ((((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝒫 𝑣 = 𝒫 𝑔) |
26 | 23, 25 | cbvrexdva2 3152 |
. . . . . . . 8
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼))) |
27 | 16, 26 | imbi12d 333 |
. . . . . . 7
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)) ↔ (((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)))) |
28 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑡 = ℎ ∧ 𝑢 = 𝑓) → 𝑡 = ℎ) |
29 | 28 | difeq2d 3690 |
. . . . . . . . 9
⊢ ((𝑡 = ℎ ∧ 𝑢 = 𝑓) → (𝑋 ∖ 𝑡) = (𝑋 ∖ ℎ)) |
30 | 29 | pweqd 4113 |
. . . . . . . 8
⊢ ((𝑡 = ℎ ∧ 𝑢 = 𝑓) → 𝒫 (𝑋 ∖ 𝑡) = 𝒫 (𝑋 ∖ ℎ)) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ (((𝑡 = ℎ ∧ 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝒫 (𝑋 ∖ 𝑡) = 𝒫 (𝑋 ∖ ℎ)) |
32 | 27, 31 | cbvraldva2 3151 |
. . . . . 6
⊢ ((𝑡 = ℎ ∧ 𝑢 = 𝑓) → (∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)) ↔ ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)))) |
33 | 32, 30 | cbvraldva2 3151 |
. . . . 5
⊢ (𝑡 = ℎ → (∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)))) |
34 | 33 | cbvalv 2261 |
. . . 4
⊢
(∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼))) |
35 | 4, 34 | sylib 207 |
. . 3
⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼))) |
36 | | ssun2 3739 |
. . . . . 6
⊢ 𝐻 ⊆ (𝐹 ∪ 𝐻) |
37 | 36 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐻 ⊆ (𝐹 ∪ 𝐻)) |
38 | 3, 37 | ssexd 4733 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ V) |
39 | | mreexexlemd.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) |
40 | | mreexexlemd.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
41 | | difexg 4735 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐽 → (𝑋 ∖ 𝐻) ∈ V) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∖ 𝐻) ∈ V) |
43 | 42, 39 | ssexd 4733 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) |
44 | | elpwg 4116 |
. . . . . . . . 9
⊢ (𝐹 ∈ V → (𝐹 ∈ 𝒫 (𝑋 ∖ 𝐻) ↔ 𝐹 ⊆ (𝑋 ∖ 𝐻))) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∈ 𝒫 (𝑋 ∖ 𝐻) ↔ 𝐹 ⊆ (𝑋 ∖ 𝐻))) |
46 | 39, 45 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝒫 (𝑋 ∖ 𝐻)) |
47 | 46 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ = 𝐻) → 𝐹 ∈ 𝒫 (𝑋 ∖ 𝐻)) |
48 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ ℎ = 𝐻) → ℎ = 𝐻) |
49 | 48 | difeq2d 3690 |
. . . . . . 7
⊢ ((𝜑 ∧ ℎ = 𝐻) → (𝑋 ∖ ℎ) = (𝑋 ∖ 𝐻)) |
50 | 49 | pweqd 4113 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ = 𝐻) → 𝒫 (𝑋 ∖ ℎ) = 𝒫 (𝑋 ∖ 𝐻)) |
51 | 47, 50 | eleqtrrd 2691 |
. . . . 5
⊢ ((𝜑 ∧ ℎ = 𝐻) → 𝐹 ∈ 𝒫 (𝑋 ∖ ℎ)) |
52 | | mreexexlemd.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) |
53 | 42, 52 | ssexd 4733 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ V) |
54 | | elpwg 4116 |
. . . . . . . . . 10
⊢ (𝐺 ∈ V → (𝐺 ∈ 𝒫 (𝑋 ∖ 𝐻) ↔ 𝐺 ⊆ (𝑋 ∖ 𝐻))) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ 𝒫 (𝑋 ∖ 𝐻) ↔ 𝐺 ⊆ (𝑋 ∖ 𝐻))) |
56 | 52, 55 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝒫 (𝑋 ∖ 𝐻)) |
57 | 56 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋 ∖ 𝐻)) |
58 | 50 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) → 𝒫 (𝑋 ∖ ℎ) = 𝒫 (𝑋 ∖ 𝐻)) |
59 | 57, 58 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋 ∖ ℎ)) |
60 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹) |
61 | 60 | breq1d 4593 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ≈ 𝐾 ↔ 𝐹 ≈ 𝐾)) |
62 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
63 | 62 | breq1d 4593 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔 ≈ 𝐾 ↔ 𝐺 ≈ 𝐾)) |
64 | 61, 63 | orbi12d 742 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ↔ (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾))) |
65 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ℎ = 𝐻) |
66 | 62, 65 | uneq12d 3730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔 ∪ ℎ) = (𝐺 ∪ 𝐻)) |
67 | 66 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑁‘(𝑔 ∪ ℎ)) = (𝑁‘(𝐺 ∪ 𝐻))) |
68 | 60, 67 | sseq12d 3597 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ↔ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))) |
69 | 60, 65 | uneq12d 3730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ∪ ℎ) = (𝐹 ∪ 𝐻)) |
70 | 69 | eleq1d 2672 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓 ∪ ℎ) ∈ 𝐼 ↔ (𝐹 ∪ 𝐻) ∈ 𝐼)) |
71 | 64, 68, 70 | 3anbi123d 1391 |
. . . . . . 7
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)) ∧ (𝐹 ∪ 𝐻) ∈ 𝐼))) |
72 | 62 | pweqd 4113 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝒫 𝑔 = 𝒫 𝐺) |
73 | 60 | breq1d 4593 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ≈ 𝑗 ↔ 𝐹 ≈ 𝑗)) |
74 | 65 | uneq2d 3729 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑗 ∪ ℎ) = (𝑗 ∪ 𝐻)) |
75 | 74 | eleq1d 2672 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑗 ∪ ℎ) ∈ 𝐼 ↔ (𝑗 ∪ 𝐻) ∈ 𝐼)) |
76 | 73, 75 | anbi12d 743 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼) ↔ (𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))) |
77 | 72, 76 | rexeqbidv 3130 |
. . . . . . 7
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))) |
78 | 71, 77 | imbi12d 333 |
. . . . . 6
⊢ ((((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)) ↔ (((𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)) ∧ (𝐹 ∪ 𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)))) |
79 | 59, 78 | rspcdv 3285 |
. . . . 5
⊢ (((𝜑 ∧ ℎ = 𝐻) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)) → (((𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)) ∧ (𝐹 ∪ 𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)))) |
80 | 51, 79 | rspcimdv 3283 |
. . . 4
⊢ ((𝜑 ∧ ℎ = 𝐻) → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)) → (((𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)) ∧ (𝐹 ∪ 𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)))) |
81 | 38, 80 | spcimdv 3263 |
. . 3
⊢ (𝜑 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)) → (((𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)) ∧ (𝐹 ∪ 𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)))) |
82 | 35, 81 | mpd 15 |
. 2
⊢ (𝜑 → (((𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)) ∧ (𝐹 ∪ 𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))) |
83 | 1, 2, 3, 82 | mp3and 1419 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)) |