MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz7.49 Structured version   Visualization version   GIF version

Theorem tz7.49 8485
Description: Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.)
Hypotheses
Ref Expression
tz7.49.1 𝐹 Fn On
tz7.49.2 (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
Assertion
Ref Expression
tz7.49 ((𝐴𝐵𝜑) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem tz7.49
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-ne 2941 . . . . . . . . 9 ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
21ralbii 3093 . . . . . . . 8 (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
3 tz7.49.2 . . . . . . . . 9 (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
4 ralim 3086 . . . . . . . . 9 (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
53, 4sylbi 217 . . . . . . . 8 (𝜑 → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
62, 5biimtrrid 243 . . . . . . 7 (𝜑 → (∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
7 tz7.49.1 . . . . . . . . 9 𝐹 Fn On
87tz7.48-3 8484 . . . . . . . 8 (∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) → ¬ 𝐴 ∈ V)
9 elex 3501 . . . . . . . 8 (𝐴𝐵𝐴 ∈ V)
108, 9nsyl3 138 . . . . . . 7 (𝐴𝐵 → ¬ ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
116, 10nsyli 157 . . . . . 6 (𝜑 → (𝐴𝐵 → ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅))
12 dfrex2 3073 . . . . . 6 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ ↔ ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
1311, 12imbitrrdi 252 . . . . 5 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅))
14 imaeq2 6074 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
1514difeq2d 4126 . . . . . . 7 (𝑥 = 𝑦 → (𝐴 ∖ (𝐹𝑥)) = (𝐴 ∖ (𝐹𝑦)))
1615eqeq1d 2739 . . . . . 6 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) = ∅ ↔ (𝐴 ∖ (𝐹𝑦)) = ∅))
1716onminex 7822 . . . . 5 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
1813, 17syl6 35 . . . 4 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)))
19 df-ne 2941 . . . . . . 7 ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2019ralbii 3093 . . . . . 6 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2120anbi2i 623 . . . . 5 (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2221rexbii 3094 . . . 4 (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2318, 22imbitrrdi 252 . . 3 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
24 nfra1 3284 . . . . 5 𝑥𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
253, 24nfxfr 1853 . . . 4 𝑥𝜑
26 simpllr 776 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
27 fnfun 6668 . . . . . . . . . . . . . . . . 17 (𝐹 Fn On → Fun 𝐹)
287, 27ax-mp 5 . . . . . . . . . . . . . . . 16 Fun 𝐹
29 fvelima 6974 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑧 ∈ (𝐹𝑥)) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
3028, 29mpan 690 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐹𝑥) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
31 nfv 1914 . . . . . . . . . . . . . . . . 17 𝑦𝜑
32 nfra1 3284 . . . . . . . . . . . . . . . . 17 𝑦𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅
3331, 32nfan 1899 . . . . . . . . . . . . . . . 16 𝑦(𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
34 nfv 1914 . . . . . . . . . . . . . . . 16 𝑦(𝑥 ∈ On → 𝑧𝐴)
35 rsp 3247 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑦𝑥 → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
3635adantld 490 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
37 onelon 6409 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
3815neeq1d 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
39 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4039, 15eleq12d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) ↔ (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4138, 40imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → (((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) ↔ ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4241rspcv 3618 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
433, 42biimtrid 242 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (𝜑 → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4443com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4537, 44syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4636, 45sylcom 30 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4746com3r 87 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4847imp 406 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4948expcomd 416 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
50 eldifi 4131 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → (𝐹𝑦) ∈ 𝐴)
51 eleq1 2829 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝐴𝑧𝐴))
5250, 51syl5ibcom 245 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑦) = 𝑧𝑧𝐴))
5349, 52syl8 76 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → ((𝐹𝑦) = 𝑧𝑧𝐴))))
5453com34 91 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → ((𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴))))
5533, 34, 54rexlimd 3266 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∃𝑦𝑥 (𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴)))
5630, 55syl5 34 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑧 ∈ (𝐹𝑥) → (𝑥 ∈ On → 𝑧𝐴)))
5756com23 86 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴)))
5857imp 406 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴))
5958ssrdv 3989 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝐹𝑥) ⊆ 𝐴)
60 ssdif0 4366 . . . . . . . . . . . 12 (𝐴 ⊆ (𝐹𝑥) ↔ (𝐴 ∖ (𝐹𝑥)) = ∅)
6160biimpri 228 . . . . . . . . . . 11 ((𝐴 ∖ (𝐹𝑥)) = ∅ → 𝐴 ⊆ (𝐹𝑥))
6259, 61anim12i 613 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
63 eqss 3999 . . . . . . . . . 10 ((𝐹𝑥) = 𝐴 ↔ ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
6462, 63sylibr 234 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (𝐹𝑥) = 𝐴)
65 onss 7805 . . . . . . . . . . . . 13 (𝑥 ∈ On → 𝑥 ⊆ On)
6632, 31nfan 1899 . . . . . . . . . . . . . . . . 17 𝑦(∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑)
67 nfv 1914 . . . . . . . . . . . . . . . . 17 𝑦 𝑥 ⊆ On
6866, 67nfan 1899 . . . . . . . . . . . . . . . 16 𝑦((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On)
69 nfv 1914 . . . . . . . . . . . . . . . . . 18 𝑧(((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥)
70 ssel 3977 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥𝑦 ∈ On))
71 onss 7805 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → 𝑦 ⊆ On)
727fndmi 6672 . . . . . . . . . . . . . . . . . . . . . . . 24 dom 𝐹 = On
7371, 72sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → 𝑦 ⊆ dom 𝐹)
74 funfvima2 7251 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7528, 73, 74sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ On → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7670, 75syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦))))
7735com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
7970, 78, 44syl10 79 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))))
8079imp4a 422 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
81 eldifn 4132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ¬ (𝐹𝑦) ∈ (𝐹𝑦))
82 eleq1a 2836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑧) ∈ (𝐹𝑦) → ((𝐹𝑦) = (𝐹𝑧) → (𝐹𝑦) ∈ (𝐹𝑦)))
8382con3d 152 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑧) ∈ (𝐹𝑦) → (¬ (𝐹𝑦) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8481, 83syl5com 31 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8580, 84syl8 76 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8685com34 91 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → ((𝐹𝑧) ∈ (𝐹𝑦) → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8776, 86syldd 72 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8887com4r 94 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8988imp31 417 . . . . . . . . . . . . . . . . . 18 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))
9069, 89ralrimi 3257 . . . . . . . . . . . . . . . . 17 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9190ex 412 . . . . . . . . . . . . . . . 16 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → (𝑦𝑥 → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9268, 91ralrimi 3257 . . . . . . . . . . . . . . 15 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9392ex 412 . . . . . . . . . . . . . 14 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9493ancld 550 . . . . . . . . . . . . 13 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))))
957tz7.48lem 8481 . . . . . . . . . . . . 13 ((𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)) → Fun (𝐹𝑥))
9665, 94, 95syl56 36 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9796ancoms 458 . . . . . . . . . . 11 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9897imp 406 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → Fun (𝐹𝑥))
9998adantr 480 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → Fun (𝐹𝑥))
10026, 64, 993jca 1129 . . . . . . . 8 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
101100exp41 434 . . . . . . 7 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
102101com23 86 . . . . . 6 (𝜑 → (𝑥 ∈ On → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
103102com34 91 . . . . 5 (𝜑 → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
104103imp4a 422 . . . 4 (𝜑 → (𝑥 ∈ On → (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))))
10525, 104reximdai 3261 . . 3 (𝜑 → (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
10623, 105syld 47 . 2 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
107106impcom 407 1 ((𝐴𝐵𝜑) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cdif 3948  wss 3951  c0 4333  ccnv 5684  dom cdm 5685  cres 5687  cima 5688  Oncon0 6384  Fun wfun 6555   Fn wfn 6556  cfv 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569
This theorem is referenced by:  tz7.49c  8486
  Copyright terms: Public domain W3C validator