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 8068
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 2991 . . . . . . . . 9 ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
21ralbii 3136 . . . . . . . 8 (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
3 tz7.49.2 . . . . . . . . 9 (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
4 ralim 3133 . . . . . . . . 9 (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
53, 4sylbi 220 . . . . . . . 8 (𝜑 → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
62, 5syl5bir 246 . . . . . . 7 (𝜑 → (∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
7 tz7.49.1 . . . . . . . . 9 𝐹 Fn On
87tz7.48-3 8067 . . . . . . . 8 (∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) → ¬ 𝐴 ∈ V)
9 elex 3462 . . . . . . . 8 (𝐴𝐵𝐴 ∈ V)
108, 9nsyl3 140 . . . . . . 7 (𝐴𝐵 → ¬ ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
116, 10nsyli 160 . . . . . 6 (𝜑 → (𝐴𝐵 → ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅))
12 dfrex2 3205 . . . . . 6 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ ↔ ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
1311, 12syl6ibr 255 . . . . 5 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅))
14 imaeq2 5896 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
1514difeq2d 4053 . . . . . . 7 (𝑥 = 𝑦 → (𝐴 ∖ (𝐹𝑥)) = (𝐴 ∖ (𝐹𝑦)))
1615eqeq1d 2803 . . . . . 6 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) = ∅ ↔ (𝐴 ∖ (𝐹𝑦)) = ∅))
1716onminex 7506 . . . . 5 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
1813, 17syl6 35 . . . 4 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)))
19 df-ne 2991 . . . . . . 7 ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2019ralbii 3136 . . . . . 6 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2120anbi2i 625 . . . . 5 (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2221rexbii 3213 . . . 4 (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2318, 22syl6ibr 255 . . 3 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
24 nfra1 3186 . . . . 5 𝑥𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
253, 24nfxfr 1854 . . . 4 𝑥𝜑
26 simpllr 775 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
27 fnfun 6427 . . . . . . . . . . . . . . . . 17 (𝐹 Fn On → Fun 𝐹)
287, 27ax-mp 5 . . . . . . . . . . . . . . . 16 Fun 𝐹
29 fvelima 6710 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑧 ∈ (𝐹𝑥)) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
3028, 29mpan 689 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐹𝑥) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
31 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑦𝜑
32 nfra1 3186 . . . . . . . . . . . . . . . . 17 𝑦𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅
3331, 32nfan 1900 . . . . . . . . . . . . . . . 16 𝑦(𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
34 nfv 1915 . . . . . . . . . . . . . . . 16 𝑦(𝑥 ∈ On → 𝑧𝐴)
35 rsp 3173 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑦𝑥 → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
3635adantld 494 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
37 onelon 6188 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
3815neeq1d 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
39 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4039, 15eleq12d 2887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) ↔ (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4138, 40imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → (((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) ↔ ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4241rspcv 3569 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
433, 42syl5bi 245 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (𝜑 → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4443com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4537, 44syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4636, 45sylcom 30 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4746com3r 87 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4847imp 410 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4948expcomd 420 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
50 eldifi 4057 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → (𝐹𝑦) ∈ 𝐴)
51 eleq1 2880 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝐴𝑧𝐴))
5250, 51syl5ibcom 248 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑦) = 𝑧𝑧𝐴))
5349, 52syl8 76 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → ((𝐹𝑦) = 𝑧𝑧𝐴))))
5453com34 91 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → ((𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴))))
5533, 34, 54rexlimd 3279 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∃𝑦𝑥 (𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴)))
5630, 55syl5 34 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑧 ∈ (𝐹𝑥) → (𝑥 ∈ On → 𝑧𝐴)))
5756com23 86 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴)))
5857imp 410 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴))
5958ssrdv 3924 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝐹𝑥) ⊆ 𝐴)
60 ssdif0 4280 . . . . . . . . . . . 12 (𝐴 ⊆ (𝐹𝑥) ↔ (𝐴 ∖ (𝐹𝑥)) = ∅)
6160biimpri 231 . . . . . . . . . . 11 ((𝐴 ∖ (𝐹𝑥)) = ∅ → 𝐴 ⊆ (𝐹𝑥))
6259, 61anim12i 615 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
63 eqss 3933 . . . . . . . . . 10 ((𝐹𝑥) = 𝐴 ↔ ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
6462, 63sylibr 237 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (𝐹𝑥) = 𝐴)
65 onss 7489 . . . . . . . . . . . . 13 (𝑥 ∈ On → 𝑥 ⊆ On)
6632, 31nfan 1900 . . . . . . . . . . . . . . . . 17 𝑦(∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑)
67 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑦 𝑥 ⊆ On
6866, 67nfan 1900 . . . . . . . . . . . . . . . 16 𝑦((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On)
69 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑧(((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥)
70 ssel 3911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥𝑦 ∈ On))
71 onss 7489 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → 𝑦 ⊆ On)
727fndmi 6430 . . . . . . . . . . . . . . . . . . . . . . . 24 dom 𝐹 = On
7371, 72sseqtrrdi 3969 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → 𝑦 ⊆ dom 𝐹)
74 funfvima2 6975 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7528, 73, 74sylancr 590 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ On → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7670, 75syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦))))
7735com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
7970, 78, 44syl10 79 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))))
8079imp4a 426 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
81 eldifn 4058 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ¬ (𝐹𝑦) ∈ (𝐹𝑦))
82 eleq1a 2888 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑧) ∈ (𝐹𝑦) → ((𝐹𝑦) = (𝐹𝑧) → (𝐹𝑦) ∈ (𝐹𝑦)))
8382con3d 155 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑧) ∈ (𝐹𝑦) → (¬ (𝐹𝑦) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8481, 83syl5com 31 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8580, 84syl8 76 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8685com34 91 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → ((𝐹𝑧) ∈ (𝐹𝑦) → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8776, 86syldd 72 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8887com4r 94 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8988imp31 421 . . . . . . . . . . . . . . . . . 18 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))
9069, 89ralrimi 3183 . . . . . . . . . . . . . . . . 17 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9190ex 416 . . . . . . . . . . . . . . . 16 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → (𝑦𝑥 → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9268, 91ralrimi 3183 . . . . . . . . . . . . . . 15 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9392ex 416 . . . . . . . . . . . . . 14 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9493ancld 554 . . . . . . . . . . . . 13 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))))
957tz7.48lem 8064 . . . . . . . . . . . . 13 ((𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)) → Fun (𝐹𝑥))
9665, 94, 95syl56 36 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9796ancoms 462 . . . . . . . . . . 11 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9897imp 410 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → Fun (𝐹𝑥))
9998adantr 484 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → Fun (𝐹𝑥))
10026, 64, 993jca 1125 . . . . . . . 8 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
101100exp41 438 . . . . . . 7 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
102101com23 86 . . . . . 6 (𝜑 → (𝑥 ∈ On → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
103102com34 91 . . . . 5 (𝜑 → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
104103imp4a 426 . . . 4 (𝜑 → (𝑥 ∈ On → (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))))
10525, 104reximdai 3273 . . 3 (𝜑 → (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
10623, 105syld 47 . 2 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
107106impcom 411 1 ((𝐴𝐵𝜑) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wral 3109  wrex 3110  Vcvv 3444  cdif 3881  wss 3884  c0 4246  ccnv 5522  dom cdm 5523  cres 5525  cima 5526  Oncon0 6163  Fun wfun 6322   Fn wfn 6323  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-ord 6166  df-on 6167  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336
This theorem is referenced by:  tz7.49c  8069
  Copyright terms: Public domain W3C validator