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