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 7937
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 2985 . . . . . . . . 9 ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
21ralbii 3132 . . . . . . . 8 (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
3 tz7.49.2 . . . . . . . . 9 (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
4 ralim 3129 . . . . . . . . 9 (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
53, 4sylbi 218 . . . . . . . 8 (𝜑 → (∀𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
62, 5syl5bir 244 . . . . . . 7 (𝜑 → (∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅ → ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))))
7 tz7.49.1 . . . . . . . . 9 𝐹 Fn On
87tz7.48-3 7936 . . . . . . . 8 (∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) → ¬ 𝐴 ∈ V)
9 elex 3455 . . . . . . . 8 (𝐴𝐵𝐴 ∈ V)
108, 9nsyl3 140 . . . . . . 7 (𝐴𝐵 → ¬ ∀𝑥 ∈ On (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
116, 10nsyli 160 . . . . . 6 (𝜑 → (𝐴𝐵 → ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅))
12 dfrex2 3203 . . . . . 6 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ ↔ ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹𝑥)) = ∅)
1311, 12syl6ibr 253 . . . . 5 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅))
14 imaeq2 5807 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
1514difeq2d 4024 . . . . . . 7 (𝑥 = 𝑦 → (𝐴 ∖ (𝐹𝑥)) = (𝐴 ∖ (𝐹𝑦)))
1615eqeq1d 2797 . . . . . 6 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) = ∅ ↔ (𝐴 ∖ (𝐹𝑦)) = ∅))
1716onminex 7383 . . . . 5 (∃𝑥 ∈ On (𝐴 ∖ (𝐹𝑥)) = ∅ → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
1813, 17syl6 35 . . . 4 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)))
19 df-ne 2985 . . . . . . 7 ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2019ralbii 3132 . . . . . 6 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ↔ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅)
2120anbi2i 622 . . . . 5 (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2221rexbii 3211 . . . 4 (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ↔ ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 ¬ (𝐴 ∖ (𝐹𝑦)) = ∅))
2318, 22syl6ibr 253 . . 3 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
24 nfra1 3186 . . . . 5 𝑥𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)))
253, 24nfxfr 1834 . . . 4 𝑥𝜑
26 simpllr 772 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
27 fnfun 6328 . . . . . . . . . . . . . . . . 17 (𝐹 Fn On → Fun 𝐹)
287, 27ax-mp 5 . . . . . . . . . . . . . . . 16 Fun 𝐹
29 fvelima 6604 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑧 ∈ (𝐹𝑥)) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
3028, 29mpan 686 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐹𝑥) → ∃𝑦𝑥 (𝐹𝑦) = 𝑧)
31 nfv 1892 . . . . . . . . . . . . . . . . 17 𝑦𝜑
32 nfra1 3186 . . . . . . . . . . . . . . . . 17 𝑦𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅
3331, 32nfan 1881 . . . . . . . . . . . . . . . 16 𝑦(𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅)
34 nfv 1892 . . . . . . . . . . . . . . . 16 𝑦(𝑥 ∈ On → 𝑧𝐴)
35 rsp 3172 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑦𝑥 → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
3635adantld 491 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
37 onelon 6096 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
3815neeq1d 3043 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ ↔ (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
39 fveq2 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4039, 15eleq12d 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥)) ↔ (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4138, 40imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → (((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) ↔ ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4241rspcv 3555 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) ≠ ∅ → (𝐹𝑥) ∈ (𝐴 ∖ (𝐹𝑥))) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
433, 42syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (𝜑 → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4443com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4537, 44syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4636, 45sylcom 30 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4746com3r 87 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
4847imp 407 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))
4948expcomd 417 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
50 eldifi 4028 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → (𝐹𝑦) ∈ 𝐴)
51 eleq1 2870 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝐴𝑧𝐴))
5250, 51syl5ibcom 246 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑦) = 𝑧𝑧𝐴))
5349, 52syl8 76 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → (𝑥 ∈ On → ((𝐹𝑦) = 𝑧𝑧𝐴))))
5453com34 91 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑦𝑥 → ((𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴))))
5533, 34, 54rexlimd 3278 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∃𝑦𝑥 (𝐹𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧𝐴)))
5630, 55syl5 34 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑧 ∈ (𝐹𝑥) → (𝑥 ∈ On → 𝑧𝐴)))
5756com23 86 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴)))
5857imp 407 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝑧 ∈ (𝐹𝑥) → 𝑧𝐴))
5958ssrdv 3899 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝐹𝑥) ⊆ 𝐴)
60 ssdif0 4247 . . . . . . . . . . . 12 (𝐴 ⊆ (𝐹𝑥) ↔ (𝐴 ∖ (𝐹𝑥)) = ∅)
6160biimpri 229 . . . . . . . . . . 11 ((𝐴 ∖ (𝐹𝑥)) = ∅ → 𝐴 ⊆ (𝐹𝑥))
6259, 61anim12i 612 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
63 eqss 3908 . . . . . . . . . 10 ((𝐹𝑥) = 𝐴 ↔ ((𝐹𝑥) ⊆ 𝐴𝐴 ⊆ (𝐹𝑥)))
6462, 63sylibr 235 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (𝐹𝑥) = 𝐴)
65 onss 7366 . . . . . . . . . . . . 13 (𝑥 ∈ On → 𝑥 ⊆ On)
6632, 31nfan 1881 . . . . . . . . . . . . . . . . 17 𝑦(∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑)
67 nfv 1892 . . . . . . . . . . . . . . . . 17 𝑦 𝑥 ⊆ On
6866, 67nfan 1881 . . . . . . . . . . . . . . . 16 𝑦((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On)
69 nfv 1892 . . . . . . . . . . . . . . . . . 18 𝑧(((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥)
70 ssel 3887 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥𝑦 ∈ On))
71 onss 7366 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → 𝑦 ⊆ On)
72 fndm 6330 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 Fn On → dom 𝐹 = On)
737, 72ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 dom 𝐹 = On
7471, 73syl6sseqr 3943 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → 𝑦 ⊆ dom 𝐹)
75 funfvima2 6864 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7628, 74, 75sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ On → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦)))
7770, 76syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → (𝐹𝑧) ∈ (𝐹𝑦))))
7835com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅))
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹𝑦)) ≠ ∅)))
8070, 79, 44syl10 79 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ⊆ On → (𝑦𝑥 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝜑 → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦))))))
8180imp4a 423 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)))))
82 eldifn 4029 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ¬ (𝐹𝑦) ∈ (𝐹𝑦))
83 eleq1a 2878 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑧) ∈ (𝐹𝑦) → ((𝐹𝑦) = (𝐹𝑧) → (𝐹𝑦) ∈ (𝐹𝑦)))
8483con3d 155 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑧) ∈ (𝐹𝑦) → (¬ (𝐹𝑦) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8582, 84syl5com 31 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑦) ∈ (𝐴 ∖ (𝐹𝑦)) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))
8681, 85syl8 76 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ On → (𝑦𝑥 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ((𝐹𝑧) ∈ (𝐹𝑦) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8786com34 91 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ⊆ On → (𝑦𝑥 → ((𝐹𝑧) ∈ (𝐹𝑦) → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8877, 87syldd 72 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹𝑦) = (𝐹𝑧)))))
8988com4r 94 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑦𝑥 → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))))
9089imp31 418 . . . . . . . . . . . . . . . . . 18 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → (𝑧𝑦 → ¬ (𝐹𝑦) = (𝐹𝑧)))
9169, 90ralrimi 3183 . . . . . . . . . . . . . . . . 17 ((((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦𝑥) → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9291ex 413 . . . . . . . . . . . . . . . 16 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → (𝑦𝑥 → ∀𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9368, 92ralrimi 3183 . . . . . . . . . . . . . . 15 (((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))
9493ex 413 . . . . . . . . . . . . . 14 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)))
9594ancld 551 . . . . . . . . . . . . 13 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧))))
967tz7.48lem 7933 . . . . . . . . . . . . 13 ((𝑥 ⊆ On ∧ ∀𝑦𝑥𝑧𝑦 ¬ (𝐹𝑦) = (𝐹𝑧)) → Fun (𝐹𝑥))
9765, 95, 96syl56 36 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9897ancoms 459 . . . . . . . . . . 11 ((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (𝑥 ∈ On → Fun (𝐹𝑥)))
9998imp 407 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → Fun (𝐹𝑥))
10099adantr 481 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → Fun (𝐹𝑥))
10126, 64, 1003jca 1121 . . . . . . . 8 ((((𝜑 ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹𝑥)) = ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
102101exp41 435 . . . . . . 7 (𝜑 → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
103102com23 86 . . . . . 6 (𝜑 → (𝑥 ∈ On → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
104103com34 91 . . . . 5 (𝜑 → (𝑥 ∈ On → ((𝐴 ∖ (𝐹𝑥)) = ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))))
105104imp4a 423 . . . 4 (𝜑 → (𝑥 ∈ On → (((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))))
10625, 105reximdai 3272 . . 3 (𝜑 → (∃𝑥 ∈ On ((𝐴 ∖ (𝐹𝑥)) = ∅ ∧ ∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
10723, 106syld 47 . 2 (𝜑 → (𝐴𝐵 → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥))))
108107impcom 408 1 ((𝐴𝐵𝜑) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴 ∖ (𝐹𝑦)) ≠ ∅ ∧ (𝐹𝑥) = 𝐴 ∧ Fun (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wcel 2081  wne 2984  wral 3105  wrex 3106  Vcvv 3437  cdif 3860  wss 3863  c0 4215  ccnv 5447  dom cdm 5448  cres 5450  cima 5451  Oncon0 6071  Fun wfun 6224   Fn wfn 6225  cfv 6230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pr 5226  ax-un 7324
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-int 4787  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-ord 6074  df-on 6075  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238
This theorem is referenced by:  tz7.49c  7938
  Copyright terms: Public domain W3C validator