Metamath Proof Explorer

Theorem domunfican

Description: A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Assertion domunfican ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ensym ⊢ ( 𝐵 ≈ 𝐴 → 𝐴 ≈ 𝐵 )
2 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
3 1 2 sylib ⊢ ( 𝐵 ≈ 𝐴 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
4 ssid ⊢ 𝐴 ⊆ 𝐴
5 sseq1 ⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
6 5 anbi1d ⊢ ( 𝑎 = ∅ → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ↔ ( ∅ ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) )
7 6 anbi1d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ↔ ( ( ∅ ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) )
8 uneq1 ⊢ ( 𝑎 = ∅ → ( 𝑎 ∪ 𝑋 ) = ( ∅ ∪ 𝑋 ) )
9 imaeq2 ⊢ ( 𝑎 = ∅ → ( 𝑓 “ 𝑎 ) = ( 𝑓 “ ∅ ) )
10 9 uneq1d ⊢ ( 𝑎 = ∅ → ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) = ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) )
11 8 10 breq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ ( ∅ ∪ 𝑋 ) ≼ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) ) )
12 11 bibi1d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ↔ ( ( ∅ ∪ 𝑋 ) ≼ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
13 7 12 imbi12d ⊢ ( 𝑎 = ∅ → ( ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ↔ ( ( ( ∅ ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ∅ ∪ 𝑋 ) ≼ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
14 sseq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ⊆ 𝐴 ↔ 𝑏 ⊆ 𝐴 ) )
15 14 anbi1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ↔ ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) )
16 15 anbi1d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ↔ ( ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) )
17 uneq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∪ 𝑋 ) = ( 𝑏 ∪ 𝑋 ) )
18 imaeq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑓 “ 𝑎 ) = ( 𝑓 “ 𝑏 ) )
19 18 uneq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) = ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) )
20 17 19 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) )
21 20 bibi1d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ↔ ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
22 16 21 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ↔ ( ( ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
23 sseq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎 ⊆ 𝐴 ↔ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ) )
24 23 anbi1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ↔ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) )
25 24 anbi1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ↔ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) )
26 uneq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎 ∪ 𝑋 ) = ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) )
27 imaeq2 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑓 “ 𝑎 ) = ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) )
28 27 uneq1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) = ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) )
29 26 28 breq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ) )
30 29 bibi1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ↔ ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
31 25 30 imbi12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ↔ ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
32 sseq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
33 32 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ↔ ( 𝐴 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) )
34 33 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ↔ ( ( 𝐴 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) )
35 uneq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∪ 𝑋 ) = ( 𝐴 ∪ 𝑋 ) )
36 imaeq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑓 “ 𝑎 ) = ( 𝑓 “ 𝐴 ) )
37 36 uneq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) = ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) )
38 35 37 breq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ) )
39 38 bibi1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ↔ ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
40 34 39 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( ( 𝑎 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑎 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑎 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ↔ ( ( ( 𝐴 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
41 uncom ⊢ ( ∅ ∪ 𝑋 ) = ( 𝑋 ∪ ∅ )
42 un0 ⊢ ( 𝑋 ∪ ∅ ) = 𝑋
43 41 42 eqtri ⊢ ( ∅ ∪ 𝑋 ) = 𝑋
44 ima0 ⊢ ( 𝑓 “ ∅ ) = ∅
45 44 uneq1i ⊢ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) = ( ∅ ∪ 𝑌 )
46 uncom ⊢ ( ∅ ∪ 𝑌 ) = ( 𝑌 ∪ ∅ )
47 un0 ⊢ ( 𝑌 ∪ ∅ ) = 𝑌
48 46 47 eqtri ⊢ ( ∅ ∪ 𝑌 ) = 𝑌
49 45 48 eqtri ⊢ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) = 𝑌
50 43 49 breq12i ⊢ ( ( ∅ ∪ 𝑋 ) ≼ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 )
51 50 a1i ⊢ ( ( ( ∅ ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ∅ ∪ 𝑋 ) ≼ ( ( 𝑓 “ ∅ ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )
52 ssun1 ⊢ 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } )
53 sstr2 ⊢ ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 → 𝑏 ⊆ 𝐴 ) )
54 52 53 ax-mp ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 → 𝑏 ⊆ 𝐴 )
55 54 anim1i ⊢ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
56 55 anim1i ⊢ ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) )
57 56 imim1i ⊢ ( ( ( ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) → ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
58 uncom ⊢ ( 𝑏 ∪ { 𝑐 } ) = ( { 𝑐 } ∪ 𝑏 )
59 58 uneq1i ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) = ( ( { 𝑐 } ∪ 𝑏 ) ∪ 𝑋 )
60 unass ⊢ ( ( { 𝑐 } ∪ 𝑏 ) ∪ 𝑋 ) = ( { 𝑐 } ∪ ( 𝑏 ∪ 𝑋 ) )
61 59 60 eqtri ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) = ( { 𝑐 } ∪ ( 𝑏 ∪ 𝑋 ) )
62 61 a1i ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) = ( { 𝑐 } ∪ ( 𝑏 ∪ 𝑋 ) ) )
63 imaundi ⊢ ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) = ( ( 𝑓 “ 𝑏 ) ∪ ( 𝑓 “ { 𝑐 } ) )
64 simprlr ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
65 f1ofn ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 Fn 𝐴 )
66 64 65 syl ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → 𝑓 Fn 𝐴 )
67 ssun2 ⊢ { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } )
68 sstr2 ⊢ ( { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 → { 𝑐 } ⊆ 𝐴 ) )
69 67 68 ax-mp ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 → { 𝑐 } ⊆ 𝐴 )
70 vex ⊢ 𝑐 ∈ V
71 70 snss ⊢ ( 𝑐 ∈ 𝐴 ↔ { 𝑐 } ⊆ 𝐴 )
72 69 71 sylibr ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 → 𝑐 ∈ 𝐴 )
73 72 adantr ⊢ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝑐 ∈ 𝐴 )
74 73 ad2antrl ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → 𝑐 ∈ 𝐴 )
75 fnsnfv ⊢ ( ( 𝑓 Fn 𝐴 ∧ 𝑐 ∈ 𝐴 ) → { ( 𝑓 ‘ 𝑐 ) } = ( 𝑓 “ { 𝑐 } ) )
76 66 74 75 syl2anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → { ( 𝑓 ‘ 𝑐 ) } = ( 𝑓 “ { 𝑐 } ) )
77 76 eqcomd ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝑓 “ { 𝑐 } ) = { ( 𝑓 ‘ 𝑐 ) } )
78 77 uneq2d ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( 𝑓 “ 𝑏 ) ∪ ( 𝑓 “ { 𝑐 } ) ) = ( ( 𝑓 “ 𝑏 ) ∪ { ( 𝑓 ‘ 𝑐 ) } ) )
79 63 78 syl5eq ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) = ( ( 𝑓 “ 𝑏 ) ∪ { ( 𝑓 ‘ 𝑐 ) } ) )
80 79 uneq1d ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) = ( ( ( 𝑓 “ 𝑏 ) ∪ { ( 𝑓 ‘ 𝑐 ) } ) ∪ 𝑌 ) )
81 uncom ⊢ ( ( 𝑓 “ 𝑏 ) ∪ { ( 𝑓 ‘ 𝑐 ) } ) = ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( 𝑓 “ 𝑏 ) )
82 81 uneq1i ⊢ ( ( ( 𝑓 “ 𝑏 ) ∪ { ( 𝑓 ‘ 𝑐 ) } ) ∪ 𝑌 ) = ( ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( 𝑓 “ 𝑏 ) ) ∪ 𝑌 )
83 unass ⊢ ( ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( 𝑓 “ 𝑏 ) ) ∪ 𝑌 ) = ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) )
84 82 83 eqtri ⊢ ( ( ( 𝑓 “ 𝑏 ) ∪ { ( 𝑓 ‘ 𝑐 ) } ) ∪ 𝑌 ) = ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) )
85 80 84 eqtrdi ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) = ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) )
86 62 85 breq12d ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ ( { 𝑐 } ∪ ( 𝑏 ∪ 𝑋 ) ) ≼ ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) ) )
87 simplr ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ¬ 𝑐 ∈ 𝑏 )
88 incom ⊢ ( 𝑋 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑋 )
89 simprrl ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝐴 ∩ 𝑋 ) = ∅ )
90 88 89 syl5eq ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝑋 ∩ 𝐴 ) = ∅ )
91 minel ⊢ ( ( 𝑐 ∈ 𝐴 ∧ ( 𝑋 ∩ 𝐴 ) = ∅ ) → ¬ 𝑐 ∈ 𝑋 )
92 74 90 91 syl2anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ¬ 𝑐 ∈ 𝑋 )
93 ioran ⊢ ( ¬ ( 𝑐 ∈ 𝑏 ∨ 𝑐 ∈ 𝑋 ) ↔ ( ¬ 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑋 ) )
94 elun ⊢ ( 𝑐 ∈ ( 𝑏 ∪ 𝑋 ) ↔ ( 𝑐 ∈ 𝑏 ∨ 𝑐 ∈ 𝑋 ) )
95 93 94 xchnxbir ⊢ ( ¬ 𝑐 ∈ ( 𝑏 ∪ 𝑋 ) ↔ ( ¬ 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑋 ) )
96 87 92 95 sylanbrc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ¬ 𝑐 ∈ ( 𝑏 ∪ 𝑋 ) )
97 simplr ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) → ¬ 𝑐 ∈ 𝑏 )
98 f1of1 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –1-1→ 𝐵 )
99 98 adantl ⊢ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
100 54 adantr ⊢ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝑏 ⊆ 𝐴 )
101 f1elima ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑐 ∈ 𝐴 ∧ 𝑏 ⊆ 𝐴 ) → ( ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) ↔ 𝑐 ∈ 𝑏 ) )
102 99 73 100 101 syl3anc ⊢ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) ↔ 𝑐 ∈ 𝑏 ) )
103 102 biimpd ⊢ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) → 𝑐 ∈ 𝑏 ) )
104 103 adantl ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) → 𝑐 ∈ 𝑏 ) )
105 97 104 mtod ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ) → ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) )
106 105 adantrr ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) )
107 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
108 64 107 syl ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → 𝑓 : 𝐴 ⟶ 𝐵 )
109 108 74 ffvelrnd ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝑓 ‘ 𝑐 ) ∈ 𝐵 )
110 incom ⊢ ( 𝑌 ∩ 𝐵 ) = ( 𝐵 ∩ 𝑌 )
111 simprrr ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝐵 ∩ 𝑌 ) = ∅ )
112 110 111 syl5eq ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( 𝑌 ∩ 𝐵 ) = ∅ )
113 minel ⊢ ( ( ( 𝑓 ‘ 𝑐 ) ∈ 𝐵 ∧ ( 𝑌 ∩ 𝐵 ) = ∅ ) → ¬ ( 𝑓 ‘ 𝑐 ) ∈ 𝑌 )
114 109 112 113 syl2anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ¬ ( 𝑓 ‘ 𝑐 ) ∈ 𝑌 )
115 ioran ⊢ ( ¬ ( ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) ∨ ( 𝑓 ‘ 𝑐 ) ∈ 𝑌 ) ↔ ( ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) ∧ ¬ ( 𝑓 ‘ 𝑐 ) ∈ 𝑌 ) )
116 elun ⊢ ( ( 𝑓 ‘ 𝑐 ) ∈ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ ( ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) ∨ ( 𝑓 ‘ 𝑐 ) ∈ 𝑌 ) )
117 115 116 xchnxbir ⊢ ( ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ ( ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑓 “ 𝑏 ) ∧ ¬ ( 𝑓 ‘ 𝑐 ) ∈ 𝑌 ) )
118 106 114 117 sylanbrc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) )
119 fvex ⊢ ( 𝑓 ‘ 𝑐 ) ∈ V
120 70 119 domunsncan ⊢ ( ( ¬ 𝑐 ∈ ( 𝑏 ∪ 𝑋 ) ∧ ¬ ( 𝑓 ‘ 𝑐 ) ∈ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) → ( ( { 𝑐 } ∪ ( 𝑏 ∪ 𝑋 ) ) ≼ ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) ↔ ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) )
121 96 118 120 syl2anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( { 𝑐 } ∪ ( 𝑏 ∪ 𝑋 ) ) ≼ ( { ( 𝑓 ‘ 𝑐 ) } ∪ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) ↔ ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) )
122 86 121 bitrd ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) )
123 bitr ⊢ ( ( ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) ∧ ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )
124 123 ex ⊢ ( ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ) → ( ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
125 122 124 syl ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) ) → ( ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
126 125 ex ⊢ ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
127 126 a2d ⊢ ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) → ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
128 57 127 syl5 ⊢ ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( ( ( 𝑏 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝑏 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝑏 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) → ( ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ∪ 𝑋 ) ≼ ( ( 𝑓 “ ( 𝑏 ∪ { 𝑐 } ) ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
129 13 22 31 40 51 128 findcard2s ⊢ ( 𝐴 ∈ Fin → ( ( ( 𝐴 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
130 129 expd ⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ⊆ 𝐴 ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
131 4 130 mpani ⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
132 131 3imp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )
133 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
134 foima ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( 𝑓 “ 𝐴 ) = 𝐵 )
135 133 134 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑓 “ 𝐴 ) = 𝐵 )
136 135 uneq1d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) = ( 𝐵 ∪ 𝑌 ) )
137 136 breq2d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ) )
138 137 bibi1d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ↔ ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
139 138 3ad2ant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( ( 𝐴 ∪ 𝑋 ) ≼ ( ( 𝑓 “ 𝐴 ) ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ↔ ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) )
140 132 139 mpbid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )
141 140 3exp ⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
142 141 exlimdv ⊢ ( 𝐴 ∈ Fin → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
143 3 142 syl5 ⊢ ( 𝐴 ∈ Fin → ( 𝐵 ≈ 𝐴 → ( ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) ) ) )
144 143 imp31 ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝑋 ) = ∅ ∧ ( 𝐵 ∩ 𝑌 ) = ∅ ) ) → ( ( 𝐴 ∪ 𝑋 ) ≼ ( 𝐵 ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )