Metamath Proof Explorer


Theorem tz7.49

Description: Proposition 7.49 of TakeutiZaring p. 51. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 10-Jan-2013)

Ref Expression
Hypotheses tz7.49.1 𝐹 Fn On
tz7.49.2 ( 𝜑 ↔ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) )
Assertion tz7.49 ( ( 𝐴𝐵𝜑 ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 tz7.49.1 𝐹 Fn On
2 tz7.49.2 ( 𝜑 ↔ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) )
3 df-ne ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ ↔ ¬ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ )
4 3 ralbii ( ∀ 𝑥 ∈ On ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ ↔ ∀ 𝑥 ∈ On ¬ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ )
5 ralim ( ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) → ( ∀ 𝑥 ∈ On ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ∀ 𝑥 ∈ On ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) )
6 2 5 sylbi ( 𝜑 → ( ∀ 𝑥 ∈ On ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ∀ 𝑥 ∈ On ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) )
7 4 6 syl5bir ( 𝜑 → ( ∀ 𝑥 ∈ On ¬ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ → ∀ 𝑥 ∈ On ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) )
8 1 tz7.48-3 ( ∀ 𝑥 ∈ On ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) → ¬ 𝐴 ∈ V )
9 elex ( 𝐴𝐵𝐴 ∈ V )
10 8 9 nsyl3 ( 𝐴𝐵 → ¬ ∀ 𝑥 ∈ On ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) )
11 7 10 nsyli ( 𝜑 → ( 𝐴𝐵 → ¬ ∀ 𝑥 ∈ On ¬ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) )
12 dfrex2 ( ∃ 𝑥 ∈ On ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ↔ ¬ ∀ 𝑥 ∈ On ¬ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ )
13 11 12 syl6ibr ( 𝜑 → ( 𝐴𝐵 → ∃ 𝑥 ∈ On ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) )
14 imaeq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
15 14 difeq2d ( 𝑥 = 𝑦 → ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ( 𝐴 ∖ ( 𝐹𝑦 ) ) )
16 15 eqeq1d ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ↔ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ ) )
17 16 onminex ( ∃ 𝑥 ∈ On ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ → ∃ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ¬ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ ) )
18 13 17 syl6 ( 𝜑 → ( 𝐴𝐵 → ∃ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ¬ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ ) ) )
19 df-ne ( ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ↔ ¬ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ )
20 19 ralbii ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ↔ ∀ 𝑦𝑥 ¬ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ )
21 20 anbi2i ( ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ↔ ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ¬ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ ) )
22 21 rexbii ( ∃ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ↔ ∃ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ¬ ( 𝐴 ∖ ( 𝐹𝑦 ) ) = ∅ ) )
23 18 22 syl6ibr ( 𝜑 → ( 𝐴𝐵 → ∃ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ) )
24 nfra1 𝑥𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) )
25 2 24 nfxfr 𝑥 𝜑
26 simpllr ( ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) → ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ )
27 fnfun ( 𝐹 Fn On → Fun 𝐹 )
28 1 27 ax-mp Fun 𝐹
29 fvelima ( ( Fun 𝐹𝑧 ∈ ( 𝐹𝑥 ) ) → ∃ 𝑦𝑥 ( 𝐹𝑦 ) = 𝑧 )
30 28 29 mpan ( 𝑧 ∈ ( 𝐹𝑥 ) → ∃ 𝑦𝑥 ( 𝐹𝑦 ) = 𝑧 )
31 nfv 𝑦 𝜑
32 nfra1 𝑦𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅
33 31 32 nfan 𝑦 ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ )
34 nfv 𝑦 ( 𝑥 ∈ On → 𝑧𝐴 )
35 rsp ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝑦𝑥 → ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) )
36 35 adantld ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) )
37 onelon ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → 𝑦 ∈ On )
38 15 neeq1d ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ ↔ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) )
39 fveq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
40 39 15 eleq12d ( 𝑥 = 𝑦 → ( ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ↔ ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) )
41 38 40 imbi12d ( 𝑥 = 𝑦 → ( ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) ↔ ( ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
42 41 rspcv ( 𝑦 ∈ On → ( ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) ≠ ∅ → ( 𝐹𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ) → ( ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
43 2 42 syl5bi ( 𝑦 ∈ On → ( 𝜑 → ( ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
44 43 com23 ( 𝑦 ∈ On → ( ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝜑 → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
45 37 44 syl ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → ( ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝜑 → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
46 36 45 sylcom ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → ( 𝜑 → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
47 46 com3r ( 𝜑 → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
48 47 imp ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) )
49 48 expcomd ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( 𝑦𝑥 → ( 𝑥 ∈ On → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
50 eldifi ( ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) → ( 𝐹𝑦 ) ∈ 𝐴 )
51 eleq1 ( ( 𝐹𝑦 ) = 𝑧 → ( ( 𝐹𝑦 ) ∈ 𝐴𝑧𝐴 ) )
52 50 51 syl5ibcom ( ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) → ( ( 𝐹𝑦 ) = 𝑧𝑧𝐴 ) )
53 49 52 syl8 ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( 𝑦𝑥 → ( 𝑥 ∈ On → ( ( 𝐹𝑦 ) = 𝑧𝑧𝐴 ) ) ) )
54 53 com34 ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( 𝑦𝑥 → ( ( 𝐹𝑦 ) = 𝑧 → ( 𝑥 ∈ On → 𝑧𝐴 ) ) ) )
55 33 34 54 rexlimd ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( ∃ 𝑦𝑥 ( 𝐹𝑦 ) = 𝑧 → ( 𝑥 ∈ On → 𝑧𝐴 ) ) )
56 30 55 syl5 ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( 𝑧 ∈ ( 𝐹𝑥 ) → ( 𝑥 ∈ On → 𝑧𝐴 ) ) )
57 56 com23 ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( 𝑥 ∈ On → ( 𝑧 ∈ ( 𝐹𝑥 ) → 𝑧𝐴 ) ) )
58 57 imp ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ ( 𝐹𝑥 ) → 𝑧𝐴 ) )
59 58 ssrdv ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) → ( 𝐹𝑥 ) ⊆ 𝐴 )
60 ssdif0 ( 𝐴 ⊆ ( 𝐹𝑥 ) ↔ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ )
61 60 biimpri ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ → 𝐴 ⊆ ( 𝐹𝑥 ) )
62 59 61 anim12i ( ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) → ( ( 𝐹𝑥 ) ⊆ 𝐴𝐴 ⊆ ( 𝐹𝑥 ) ) )
63 eqss ( ( 𝐹𝑥 ) = 𝐴 ↔ ( ( 𝐹𝑥 ) ⊆ 𝐴𝐴 ⊆ ( 𝐹𝑥 ) ) )
64 62 63 sylibr ( ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) → ( 𝐹𝑥 ) = 𝐴 )
65 onss ( 𝑥 ∈ On → 𝑥 ⊆ On )
66 32 31 nfan 𝑦 ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 )
67 nfv 𝑦 𝑥 ⊆ On
68 66 67 nfan 𝑦 ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) ∧ 𝑥 ⊆ On )
69 nfv 𝑧 ( ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) ∧ 𝑥 ⊆ On ) ∧ 𝑦𝑥 )
70 ssel ( 𝑥 ⊆ On → ( 𝑦𝑥𝑦 ∈ On ) )
71 onss ( 𝑦 ∈ On → 𝑦 ⊆ On )
72 1 fndmi dom 𝐹 = On
73 71 72 sseqtrrdi ( 𝑦 ∈ On → 𝑦 ⊆ dom 𝐹 )
74 funfvima2 ( ( Fun 𝐹𝑦 ⊆ dom 𝐹 ) → ( 𝑧𝑦 → ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) ) )
75 28 73 74 sylancr ( 𝑦 ∈ On → ( 𝑧𝑦 → ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) ) )
76 70 75 syl6 ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( 𝑧𝑦 → ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) ) ) )
77 35 com12 ( 𝑦𝑥 → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) )
78 77 a1i ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ) )
79 70 78 44 syl10 ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝜑 → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) ) )
80 79 imp4a ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) ) ) )
81 eldifn ( ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) → ¬ ( 𝐹𝑦 ) ∈ ( 𝐹𝑦 ) )
82 eleq1a ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) → ( ( 𝐹𝑦 ) = ( 𝐹𝑧 ) → ( 𝐹𝑦 ) ∈ ( 𝐹𝑦 ) ) )
83 82 con3d ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) → ( ¬ ( 𝐹𝑦 ) ∈ ( 𝐹𝑦 ) → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) )
84 81 83 syl5com ( ( 𝐹𝑦 ) ∈ ( 𝐴 ∖ ( 𝐹𝑦 ) ) → ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) )
85 80 84 syl8 ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) ) ) )
86 85 com34 ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑦 ) → ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) ) ) )
87 76 86 syldd ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( 𝑧𝑦 → ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) ) ) )
88 87 com4r ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ( 𝑥 ⊆ On → ( 𝑦𝑥 → ( 𝑧𝑦 → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) ) ) )
89 88 imp31 ( ( ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) ∧ 𝑥 ⊆ On ) ∧ 𝑦𝑥 ) → ( 𝑧𝑦 → ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) )
90 69 89 ralrimi ( ( ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) ∧ 𝑥 ⊆ On ) ∧ 𝑦𝑥 ) → ∀ 𝑧𝑦 ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) )
91 90 ex ( ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) ∧ 𝑥 ⊆ On ) → ( 𝑦𝑥 → ∀ 𝑧𝑦 ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) )
92 68 91 ralrimi ( ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) ∧ 𝑥 ⊆ On ) → ∀ 𝑦𝑥𝑧𝑦 ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) )
93 92 ex ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ( 𝑥 ⊆ On → ∀ 𝑦𝑥𝑧𝑦 ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) )
94 93 ancld ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ( 𝑥 ⊆ On → ( 𝑥 ⊆ On ∧ ∀ 𝑦𝑥𝑧𝑦 ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) ) )
95 1 tz7.48lem ( ( 𝑥 ⊆ On ∧ ∀ 𝑦𝑥𝑧𝑦 ¬ ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ) → Fun ( 𝐹𝑥 ) )
96 65 94 95 syl56 ( ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ 𝜑 ) → ( 𝑥 ∈ On → Fun ( 𝐹𝑥 ) ) )
97 96 ancoms ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( 𝑥 ∈ On → Fun ( 𝐹𝑥 ) ) )
98 97 imp ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) → Fun ( 𝐹𝑥 ) )
99 98 adantr ( ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) → Fun ( 𝐹𝑥 ) )
100 26 64 99 3jca ( ( ( ( 𝜑 ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ) → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) )
101 100 exp41 ( 𝜑 → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( 𝑥 ∈ On → ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) ) ) ) )
102 101 com23 ( 𝜑 → ( 𝑥 ∈ On → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) ) ) ) )
103 102 com34 ( 𝜑 → ( 𝑥 ∈ On → ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) ) ) ) )
104 103 imp4a ( 𝜑 → ( 𝑥 ∈ On → ( ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) ) ) )
105 25 104 reximdai ( 𝜑 → ( ∃ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ∅ ∧ ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) ) )
106 23 105 syld ( 𝜑 → ( 𝐴𝐵 → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) ) )
107 106 impcom ( ( 𝐴𝐵𝜑 ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴 ∖ ( 𝐹𝑦 ) ) ≠ ∅ ∧ ( 𝐹𝑥 ) = 𝐴 ∧ Fun ( 𝐹𝑥 ) ) )