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 7585
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 2824 . . . . . . . . 9 ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
21ralbii 3009 . . . . . . . 8 (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
3 tz7.49.2 . . . . . . . . 9 (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
4 ralim 2977 . . . . . . . . 9 (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
53, 4sylbi 207 . . . . . . . 8 (𝜑 → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
62, 5syl5bir 233 . . . . . . 7 (𝜑 → (∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
7 tz7.49.1 . . . . . . . . 9 𝐹 Fn On
87tz7.48-3 7584 . . . . . . . 8 (∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) → ¬ 𝐴 ∈ V)
9 elex 3243 . . . . . . . 8 (𝐴𝐵𝐴 ∈ V)
108, 9nsyl3 133 . . . . . . 7 (𝐴𝐵 → ¬ ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
116, 10nsyli 155 . . . . . 6 (𝜑 → (𝐴𝐵 → ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅))
12 dfrex2 3025 . . . . . 6 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ ↔ ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
1311, 12syl6ibr 242 . . . . 5 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅))
14 imaeq2 5497 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
1514difeq2d 3761 . . . . . . 7 (𝑥 = 𝑦 → (𝐴 ∖ (𝐹𝑥)) = (𝐴 ∖ (𝐹𝑦)))
1615eqeq1d 2653 . . . . . 6 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) = ∅ ↔ (𝐴 ∖ (𝐹𝑦)) = ∅))
1716onminex 7049 . . . . 5 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
1813, 17syl6 35 . . . 4 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)))
19 df-ne 2824 . . . . . . 7 ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2019ralbii 3009 . . . . . 6 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2120anbi2i 730 . . . . 5 (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2221rexbii 3070 . . . 4 (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2318, 22syl6ibr 242 . . 3 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
24 nfra1 2970 . . . . 5 𝑥𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
253, 24nfxfr 1819 . . . 4 𝑥𝜑
26 simpllr 815 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
27 fnfun 6026 . . . . . . . . . . . . . . . . 17 (𝐹 Fn On → Fun 𝐹)
287, 27ax-mp 5 . . . . . . . . . . . . . . . 16 Fun 𝐹
29 fvelima 6287 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑧 ∈ (𝐹𝑥)) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
3028, 29mpan 706 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐹𝑥) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
31 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑦𝜑
32 nfra1 2970 . . . . . . . . . . . . . . . . 17 𝑦𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅
3331, 32nfan 1868 . . . . . . . . . . . . . . . 16 𝑦(𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
34 nfv 1883 . . . . . . . . . . . . . . . 16 𝑦(𝑥 ∈ On → 𝑧𝐴)
35 rsp 2958 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑦𝑥 → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
3635adantld 482 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
37 onelon 5786 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
3815neeq1d 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
39 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4039, 15eleq12d 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) ↔ (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4138, 40imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → (((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) ↔ ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4241rspcv 3336 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
433, 42syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (𝜑 → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4443com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4537, 44syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4636, 45sylcom 30 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4746com3r 87 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4847imp 444 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4948expcomd 453 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
50 eldifi 3765 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → (𝐹𝑦) ∈ 𝐴)
51 eleq1 2718 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝐴𝑧𝐴))
5250, 51syl5ibcom 235 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑦) = 𝑧𝑧𝐴))
5349, 52syl8 76 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → ((𝐹𝑦) = 𝑧𝑧𝐴))))
5453com34 91 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → ((𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴))))
5533, 34, 54rexlimd 3055 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∃𝑦𝑥 (𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴)))
5630, 55syl5 34 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑧 ∈ (𝐹𝑥) → (𝑥 ∈ On → 𝑧𝐴)))
5756com23 86 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴)))
5857imp 444 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴))
5958ssrdv 3642 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝐹𝑥) ⊆ 𝐴)
60 ssdif0 3975 . . . . . . . . . . . 12 (𝐴 ⊆ (𝐹𝑥) ↔ (𝐴 ∖ (𝐹𝑥)) = ∅)
6160biimpri 218 . . . . . . . . . . 11 ((𝐴 ∖ (𝐹𝑥)) = ∅ → 𝐴 ⊆ (𝐹𝑥))
6259, 61anim12i 589 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
63 eqss 3651 . . . . . . . . . 10 ((𝐹𝑥) = 𝐴 ↔ ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
6462, 63sylibr 224 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (𝐹𝑥) = 𝐴)
65 onss 7032 . . . . . . . . . . . . 13 (𝑥 ∈ On → 𝑥 ⊆ On)
6632, 31nfan 1868 . . . . . . . . . . . . . . . . 17 𝑦(∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑)
67 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑦 𝑥 ⊆ On
6866, 67nfan 1868 . . . . . . . . . . . . . . . 16 𝑦((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On)
69 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑧(((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥)
70 ssel 3630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥𝑦 ∈ On))
71 onss 7032 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → 𝑦 ⊆ On)
72 fndm 6028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 Fn On → dom 𝐹 = On)
737, 72ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 dom 𝐹 = On
7471, 73syl6sseqr 3685 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → 𝑦 ⊆ dom 𝐹)
75 funfvima2 6533 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7628, 74, 75sylancr 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ On → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7770, 76syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦))))
7835com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
8070, 79, 44syl10 79 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))))
8180imp4a 613 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
82 eldifn 3766 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ¬ (𝐹𝑦) ∈ (𝐹𝑦))
83 eleq1a 2725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑧) ∈ (𝐹𝑦) → ((𝐹𝑦) = (𝐹𝑧) → (𝐹𝑦) ∈ (𝐹𝑦)))
8483con3d 148 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑧) ∈ (𝐹𝑦) → (¬ (𝐹𝑦) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8582, 84syl5com 31 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8681, 85syl8 76 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8786com34 91 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → ((𝐹𝑧) ∈ (𝐹𝑦) → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8877, 87syldd 72 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8988com4r 94 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))))
9089imp31 447 . . . . . . . . . . . . . . . . . 18 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))
9169, 90ralrimi 2986 . . . . . . . . . . . . . . . . 17 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9291ex 449 . . . . . . . . . . . . . . . 16 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → (𝑦𝑥 → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9368, 92ralrimi 2986 . . . . . . . . . . . . . . 15 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9493ex 449 . . . . . . . . . . . . . 14 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9594ancld 575 . . . . . . . . . . . . 13 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))))
967tz7.48lem 7581 . . . . . . . . . . . . 13 ((𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)) → Fun (𝐹𝑥))
9765, 95, 96syl56 36 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9897ancoms 468 . . . . . . . . . . 11 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9998imp 444 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → Fun (𝐹𝑥))
10099adantr 480 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → Fun (𝐹𝑥))
10126, 64, 1003jca 1261 . . . . . . . 8 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
102101exp41 637 . . . . . . 7 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
103102com23 86 . . . . . 6 (𝜑 → (𝑥 ∈ On → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
104103com34 91 . . . . 5 (𝜑 → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
105104imp4a 613 . . . 4 (𝜑 → (𝑥 ∈ On → (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))))
10625, 105reximdai 3041 . . 3 (𝜑 → (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
10723, 106syld 47 . 2 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
108107impcom 445 1 ((𝐴𝐵𝜑) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  wss 3607  c0 3948  ccnv 5142  dom cdm 5143  cres 5145  cima 5146  Oncon0 5761  Fun wfun 5920   Fn wfn 5921  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934
This theorem is referenced by:  tz7.49c  7586
  Copyright terms: Public domain W3C validator