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 ◡ ( 𝐹 ↾ 𝑥 ) ) )