Metamath Proof Explorer

Theorem fnse

Description: Condition for the well-order in fnwe to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypotheses fnse.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) }
fnse.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fnse.3 ⊢ ( 𝜑 → 𝑅 Se 𝐵 )
fnse.4 ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑤 ) ∈ V )
Assertion fnse ( 𝜑 → 𝑇 Se 𝐴 )

Proof

Step Hyp Ref Expression
1 fnse.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) }
2 fnse.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3 fnse.3 ⊢ ( 𝜑 → 𝑅 Se 𝐵 )
4 fnse.4 ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑤 ) ∈ V )
5 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
6 seex ⊢ ( ( 𝑅 Se 𝐵 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ) → { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∈ V )
7 3 5 6 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∈ V )
8 snex ⊢ { ( 𝐹 ‘ 𝑧 ) } ∈ V
9 unexg ⊢ ( ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∈ V ∧ { ( 𝐹 ‘ 𝑧 ) } ∈ V ) → ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ∈ V )
10 7 8 9 sylancl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ∈ V )
11 imaeq2 ⊢ ( 𝑤 = ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) → ( ◡ 𝐹 “ 𝑤 ) = ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) )
12 11 eleq1d ⊢ ( 𝑤 = ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) → ( ( ◡ 𝐹 “ 𝑤 ) ∈ V ↔ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ∈ V ) )
13 12 imbi2d ⊢ ( 𝑤 = ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) → ( ( 𝜑 → ( ◡ 𝐹 “ 𝑤 ) ∈ V ) ↔ ( 𝜑 → ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ∈ V ) ) )
14 13 4 vtoclg ⊢ ( ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ∈ V → ( 𝜑 → ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ∈ V ) )
15 14 impcom ⊢ ( ( 𝜑 ∧ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ∈ V ) → ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ∈ V )
16 10 15 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ∈ V )
17 inss2 ⊢ ( 𝐴 ∩ ( ◡ 𝑇 “ { 𝑧 } ) ) ⊆ ( ◡ 𝑇 “ { 𝑧 } )
18 vex ⊢ 𝑤 ∈ V
19 18 eliniseg ⊢ ( 𝑧 ∈ V → ( 𝑤 ∈ ( ◡ 𝑇 “ { 𝑧 } ) ↔ 𝑤 𝑇 𝑧 ) )
20 19 elv ⊢ ( 𝑤 ∈ ( ◡ 𝑇 “ { 𝑧 } ) ↔ 𝑤 𝑇 𝑧 )
21 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
22 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
23 21 22 breqan12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ) )
24 21 22 eqeqan12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ) )
25 breq12 ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( 𝑥 𝑆 𝑦 ↔ 𝑤 𝑆 𝑧 ) )
26 24 25 anbi12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) )
27 23 26 orbi12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) ) )
28 27 1 brab2a ⊢ ( 𝑤 𝑇 𝑧 ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) ) )
29 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
30 29 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
31 breq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑤 ) → ( 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ) )
32 31 elrab3 ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 → ( ( 𝐹 ‘ 𝑤 ) ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ) )
33 30 32 syl ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑤 ) ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ) )
34 33 biimprd ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ) )
35 fvex ⊢ ( 𝐹 ‘ 𝑤 ) ∈ V
36 35 elsn ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ { ( 𝐹 ‘ 𝑧 ) } ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
37 36 biranri ⊢ ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ { ( 𝐹 ‘ 𝑧 ) } )
38 37 a1i ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ { ( 𝐹 ‘ 𝑧 ) } ) )
39 34 38 orim12d ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) → ( ( 𝐹 ‘ 𝑤 ) ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∨ ( 𝐹 ‘ 𝑤 ) ∈ { ( 𝐹 ‘ 𝑧 ) } ) ) )
40 elun ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∨ ( 𝐹 ‘ 𝑤 ) ∈ { ( 𝐹 ‘ 𝑧 ) } ) )
41 39 40 imbitrrdi ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) )
42 simprl ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐴 )
43 41 42 jctild ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) → ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
44 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → 𝐹 Fn 𝐴 )
46 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑤 ∈ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑤 ∈ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
48 43 47 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) → 𝑤 ∈ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
49 48 expimpd ⊢ ( 𝜑 → ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 𝑆 𝑧 ) ) ) → 𝑤 ∈ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
50 28 49 biimtrid ⊢ ( 𝜑 → ( 𝑤 𝑇 𝑧 → 𝑤 ∈ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
51 20 50 biimtrid ⊢ ( 𝜑 → ( 𝑤 ∈ ( ◡ 𝑇 “ { 𝑧 } ) → 𝑤 ∈ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) ) )
52 51 ssrdv ⊢ ( 𝜑 → ( ◡ 𝑇 “ { 𝑧 } ) ⊆ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) )
53 17 52 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( ◡ 𝑇 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐴 ∩ ( ◡ 𝑇 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ ( { 𝑢 ∈ 𝐵 ∣ 𝑢 𝑅 ( 𝐹 ‘ 𝑧 ) } ∪ { ( 𝐹 ‘ 𝑧 ) } ) ) )
55 16 54 ssexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐴 ∩ ( ◡ 𝑇 “ { 𝑧 } ) ) ∈ V )
56 55 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑇 “ { 𝑧 } ) ) ∈ V )
57 dfse2 ⊢ ( 𝑇 Se 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑇 “ { 𝑧 } ) ) ∈ V )
58 56 57 sylibr ⊢ ( 𝜑 → 𝑇 Se 𝐴 )