NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nnadjoin GIF version

Theorem nnadjoin 4520
Description: Adjoining a new element to every member of L does not change its size. Theorem X.1.39 of [Rosser] p. 530. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
nnadjoin ((N Nn L N X L) → {x b L x = (b ∪ {X})} N)
Distinct variable groups:   L,b,x   X,b,x
Allowed substitution hints:   N(x,b)

Proof of Theorem nnadjoin
Dummy variables l y n a c k z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 3744 . . . . . . . . . . 11 (y = X → {y} = {X})
21uneq2d 3418 . . . . . . . . . 10 (y = X → (b ∪ {y}) = (b ∪ {X}))
32eqeq2d 2364 . . . . . . . . 9 (y = X → (x = (b ∪ {y}) ↔ x = (b ∪ {X})))
43rexbidv 2635 . . . . . . . 8 (y = X → (b L x = (b ∪ {y}) ↔ b L x = (b ∪ {X})))
54abbidv 2467 . . . . . . 7 (y = X → {x b L x = (b ∪ {y})} = {x b L x = (b ∪ {X})})
65eleq1d 2419 . . . . . 6 (y = X → ({x b L x = (b ∪ {y})} N ↔ {x b L x = (b ∪ {X})} N))
76imbi2d 307 . . . . 5 (y = X → ((L N → {x b L x = (b ∪ {y})} N) ↔ (L N → {x b L x = (b ∪ {X})} N)))
87imbi2d 307 . . . 4 (y = X → ((N Nn → (L N → {x b L x = (b ∪ {y})} N)) ↔ (N Nn → (L N → {x b L x = (b ∪ {X})} N))))
9 nnadjoinlem1 4519 . . . . . . 7 {n l n (y l → {x b l x = (b ∪ {y})} n)} V
10 eleq2 2414 . . . . . . . . . . 11 (n = 0c → ({x b l x = (b ∪ {y})} n ↔ {x b l x = (b ∪ {y})} 0c))
11 el0c 4421 . . . . . . . . . . . 12 ({x b l x = (b ∪ {y})} 0c ↔ {x b l x = (b ∪ {y})} = )
12 ab0 3569 . . . . . . . . . . . 12 ({x b l x = (b ∪ {y})} = x ¬ b l x = (b ∪ {y}))
1311, 12bitri 240 . . . . . . . . . . 11 ({x b l x = (b ∪ {y})} 0cx ¬ b l x = (b ∪ {y}))
1410, 13syl6bb 252 . . . . . . . . . 10 (n = 0c → ({x b l x = (b ∪ {y})} nx ¬ b l x = (b ∪ {y})))
1514imbi2d 307 . . . . . . . . 9 (n = 0c → ((y l → {x b l x = (b ∪ {y})} n) ↔ (y lx ¬ b l x = (b ∪ {y}))))
1615raleqbi1dv 2815 . . . . . . . 8 (n = 0c → (l n (y l → {x b l x = (b ∪ {y})} n) ↔ l 0c (y lx ¬ b l x = (b ∪ {y}))))
17 df-ral 2619 . . . . . . . . 9 (l 0c (y lx ¬ b l x = (b ∪ {y})) ↔ l(l 0c → (y lx ¬ b l x = (b ∪ {y}))))
18 el0c 4421 . . . . . . . . . . 11 (l 0cl = )
1918imbi1i 315 . . . . . . . . . 10 ((l 0c → (y lx ¬ b l x = (b ∪ {y}))) ↔ (l = → (y lx ¬ b l x = (b ∪ {y}))))
2019albii 1566 . . . . . . . . 9 (l(l 0c → (y lx ¬ b l x = (b ∪ {y}))) ↔ l(l = → (y lx ¬ b l x = (b ∪ {y}))))
21 0ex 4110 . . . . . . . . . 10 V
22 unieq 3900 . . . . . . . . . . . . 13 (l = l = )
2322compleqd 3245 . . . . . . . . . . . 12 (l = → ∼ l = ∼ )
2423eleq2d 2420 . . . . . . . . . . 11 (l = → (y ly ))
25 rexeq 2808 . . . . . . . . . . . . 13 (l = → (b l x = (b ∪ {y}) ↔ b x = (b ∪ {y})))
2625notbid 285 . . . . . . . . . . . 12 (l = → (¬ b l x = (b ∪ {y}) ↔ ¬ b x = (b ∪ {y})))
2726albidv 1625 . . . . . . . . . . 11 (l = → (x ¬ b l x = (b ∪ {y}) ↔ x ¬ b x = (b ∪ {y})))
2824, 27imbi12d 311 . . . . . . . . . 10 (l = → ((y lx ¬ b l x = (b ∪ {y})) ↔ (y x ¬ b x = (b ∪ {y}))))
2921, 28ceqsalv 2885 . . . . . . . . 9 (l(l = → (y lx ¬ b l x = (b ∪ {y}))) ↔ (y x ¬ b x = (b ∪ {y})))
3017, 20, 293bitrri 263 . . . . . . . 8 ((y x ¬ b x = (b ∪ {y})) ↔ l 0c (y lx ¬ b l x = (b ∪ {y})))
3116, 30syl6bbr 254 . . . . . . 7 (n = 0c → (l n (y l → {x b l x = (b ∪ {y})} n) ↔ (y x ¬ b x = (b ∪ {y}))))
32 eleq2 2414 . . . . . . . . 9 (n = k → ({x b l x = (b ∪ {y})} n ↔ {x b l x = (b ∪ {y})} k))
3332imbi2d 307 . . . . . . . 8 (n = k → ((y l → {x b l x = (b ∪ {y})} n) ↔ (y l → {x b l x = (b ∪ {y})} k)))
3433raleqbi1dv 2815 . . . . . . 7 (n = k → (l n (y l → {x b l x = (b ∪ {y})} n) ↔ l k (y l → {x b l x = (b ∪ {y})} k)))
35 eleq2 2414 . . . . . . . . . 10 (n = (k +c 1c) → ({x b l x = (b ∪ {y})} n ↔ {x b l x = (b ∪ {y})} (k +c 1c)))
3635imbi2d 307 . . . . . . . . 9 (n = (k +c 1c) → ((y l → {x b l x = (b ∪ {y})} n) ↔ (y l → {x b l x = (b ∪ {y})} (k +c 1c))))
3736raleqbi1dv 2815 . . . . . . . 8 (n = (k +c 1c) → (l n (y l → {x b l x = (b ∪ {y})} n) ↔ l (k +c 1c)(y l → {x b l x = (b ∪ {y})} (k +c 1c))))
38 unieq 3900 . . . . . . . . . . . 12 (l = al = a)
3938compleqd 3245 . . . . . . . . . . 11 (l = a → ∼ l = ∼ a)
4039eleq2d 2420 . . . . . . . . . 10 (l = a → (y ly a))
41 rexeq 2808 . . . . . . . . . . . 12 (l = a → (b l x = (b ∪ {y}) ↔ b a x = (b ∪ {y})))
4241abbidv 2467 . . . . . . . . . . 11 (l = a → {x b l x = (b ∪ {y})} = {x b a x = (b ∪ {y})})
4342eleq1d 2419 . . . . . . . . . 10 (l = a → ({x b l x = (b ∪ {y})} (k +c 1c) ↔ {x b a x = (b ∪ {y})} (k +c 1c)))
4440, 43imbi12d 311 . . . . . . . . 9 (l = a → ((y l → {x b l x = (b ∪ {y})} (k +c 1c)) ↔ (y a → {x b a x = (b ∪ {y})} (k +c 1c))))
4544cbvralv 2835 . . . . . . . 8 (l (k +c 1c)(y l → {x b l x = (b ∪ {y})} (k +c 1c)) ↔ a (k +c 1c)(y a → {x b a x = (b ∪ {y})} (k +c 1c)))
4637, 45syl6bb 252 . . . . . . 7 (n = (k +c 1c) → (l n (y l → {x b l x = (b ∪ {y})} n) ↔ a (k +c 1c)(y a → {x b a x = (b ∪ {y})} (k +c 1c))))
47 eleq2 2414 . . . . . . . . 9 (n = N → ({x b l x = (b ∪ {y})} n ↔ {x b l x = (b ∪ {y})} N))
4847imbi2d 307 . . . . . . . 8 (n = N → ((y l → {x b l x = (b ∪ {y})} n) ↔ (y l → {x b l x = (b ∪ {y})} N)))
4948raleqbi1dv 2815 . . . . . . 7 (n = N → (l n (y l → {x b l x = (b ∪ {y})} n) ↔ l N (y l → {x b l x = (b ∪ {y})} N)))
50 rex0 3563 . . . . . . . . 9 ¬ b x = (b ∪ {y})
5150ax-gen 1546 . . . . . . . 8 x ¬ b x = (b ∪ {y})
5251a1i 10 . . . . . . 7 (y x ¬ b x = (b ∪ {y}))
53 elsuc 4413 . . . . . . . . . 10 (a (k +c 1c) ↔ c k z ca = (c ∪ {z}))
54 unieq 3900 . . . . . . . . . . . . . . . . . . . . 21 (l = cl = c)
5554compleqd 3245 . . . . . . . . . . . . . . . . . . . 20 (l = c → ∼ l = ∼ c)
5655eleq2d 2420 . . . . . . . . . . . . . . . . . . 19 (l = c → (y ly c))
57 rexeq 2808 . . . . . . . . . . . . . . . . . . . . 21 (l = c → (b l x = (b ∪ {y}) ↔ b c x = (b ∪ {y})))
5857abbidv 2467 . . . . . . . . . . . . . . . . . . . 20 (l = c → {x b l x = (b ∪ {y})} = {x b c x = (b ∪ {y})})
5958eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (l = c → ({x b l x = (b ∪ {y})} k ↔ {x b c x = (b ∪ {y})} k))
6056, 59imbi12d 311 . . . . . . . . . . . . . . . . . 18 (l = c → ((y l → {x b l x = (b ∪ {y})} k) ↔ (y c → {x b c x = (b ∪ {y})} k)))
6160rspcv 2951 . . . . . . . . . . . . . . . . 17 (c k → (l k (y l → {x b l x = (b ∪ {y})} k) → (y c → {x b c x = (b ∪ {y})} k)))
6261adantr 451 . . . . . . . . . . . . . . . 16 ((c k z c) → (l k (y l → {x b l x = (b ∪ {y})} k) → (y c → {x b c x = (b ∪ {y})} k)))
6362adantl 452 . . . . . . . . . . . . . . 15 ((k Nn (c k z c)) → (l k (y l → {x b l x = (b ∪ {y})} k) → (y c → {x b c x = (b ∪ {y})} k)))
64 elin 3219 . . . . . . . . . . . . . . . . 17 (y ( ∼ c ∩ ∼ {z}) ↔ (y c y {z}))
65 simp3l 983 . . . . . . . . . . . . . . . . . . 19 ((k Nn (c k z c) (y c y {z})) → y c)
66 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 z V
6766unisn 3907 . . . . . . . . . . . . . . . . . . . . . . 23 {z} = z
6867compleqi 3244 . . . . . . . . . . . . . . . . . . . . . 22 {z} = ∼ z
6968eleq2i 2417 . . . . . . . . . . . . . . . . . . . . 21 (y {z} ↔ y z)
7069anbi2i 675 . . . . . . . . . . . . . . . . . . . 20 ((y c y {z}) ↔ (y c y z))
71 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22 (((k Nn (c k z c) (y c y z)) {x b c x = (b ∪ {y})} k) → {x b c x = (b ∪ {y})} k)
72 simpl2r 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((k Nn (c k z c) (y c y z)) b c) → z c)
7366elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (z c ↔ ¬ z c)
7472, 73sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((k Nn (c k z c) (y c y z)) b c) → ¬ z c)
75 eleq1a 2422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (b c → (z = bz c))
7675adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((k Nn (c k z c) (y c y z)) b c) → (z = bz c))
7774, 76mtod 168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((k Nn (c k z c) (y c y z)) b c) → ¬ z = b)
78 simpl3r 1011 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((k Nn (c k z c) (y c y z)) b c) → y z)
79 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 y V
8079elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (y z ↔ ¬ y z)
8178, 80sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((k Nn (c k z c) (y c y z)) b c) → ¬ y z)
82 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((k Nn (c k z c) (y c y z)) → y c)
8379elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (y c ↔ ¬ y c)
8482, 83sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((k Nn (c k z c) (y c y z)) → ¬ y c)
85 elunii 3896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((y b b c) → y c)
8685expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (b c → (y by c))
8786con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (b c → (¬ y c → ¬ y b))
8884, 87mpan9 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((k Nn (c k z c) (y c y z)) b c) → ¬ y b)
89 adj11 3889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ y z ¬ y b) → ((z ∪ {y}) = (b ∪ {y}) ↔ z = b))
9081, 88, 89syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((k Nn (c k z c) (y c y z)) b c) → ((z ∪ {y}) = (b ∪ {y}) ↔ z = b))
9177, 90mtbird 292 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((k Nn (c k z c) (y c y z)) b c) → ¬ (z ∪ {y}) = (b ∪ {y}))
9291nrexdv 2717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn (c k z c) (y c y z)) → ¬ b c (z ∪ {y}) = (b ∪ {y}))
93 eqeq1 2359 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (x = (z ∪ {y}) → (x = (b ∪ {y}) ↔ (z ∪ {y}) = (b ∪ {y})))
9493rexbidv 2635 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (x = (z ∪ {y}) → (b c x = (b ∪ {y}) ↔ b c (z ∪ {y}) = (b ∪ {y})))
9594elabg 2986 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((z ∪ {y}) {x b c x = (b ∪ {y})} → ((z ∪ {y}) {x b c x = (b ∪ {y})} ↔ b c (z ∪ {y}) = (b ∪ {y})))
9695ibi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 ((z ∪ {y}) {x b c x = (b ∪ {y})} → b c (z ∪ {y}) = (b ∪ {y}))
9792, 96nsyl 113 . . . . . . . . . . . . . . . . . . . . . . 23 ((k Nn (c k z c) (y c y z)) → ¬ (z ∪ {y}) {x b c x = (b ∪ {y})})
9897adantr 451 . . . . . . . . . . . . . . . . . . . . . 22 (((k Nn (c k z c) (y c y z)) {x b c x = (b ∪ {y})} k) → ¬ (z ∪ {y}) {x b c x = (b ∪ {y})})
99 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {y} V
10066, 99unex 4106 . . . . . . . . . . . . . . . . . . . . . . 23 (z ∪ {y}) V
101100elsuci 4414 . . . . . . . . . . . . . . . . . . . . . 22 (({x b c x = (b ∪ {y})} k ¬ (z ∪ {y}) {x b c x = (b ∪ {y})}) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))
10271, 98, 101syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21 (((k Nn (c k z c) (y c y z)) {x b c x = (b ∪ {y})} k) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))
103102ex 423 . . . . . . . . . . . . . . . . . . . 20 ((k Nn (c k z c) (y c y z)) → ({x b c x = (b ∪ {y})} k → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c)))
10470, 103syl3an3b 1220 . . . . . . . . . . . . . . . . . . 19 ((k Nn (c k z c) (y c y {z})) → ({x b c x = (b ∪ {y})} k → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c)))
10565, 104embantd 50 . . . . . . . . . . . . . . . . . 18 ((k Nn (c k z c) (y c y {z})) → ((y c → {x b c x = (b ∪ {y})} k) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c)))
1061053expia 1153 . . . . . . . . . . . . . . . . 17 ((k Nn (c k z c)) → ((y c y {z}) → ((y c → {x b c x = (b ∪ {y})} k) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))))
10764, 106syl5bi 208 . . . . . . . . . . . . . . . 16 ((k Nn (c k z c)) → (y ( ∼ c ∩ ∼ {z}) → ((y c → {x b c x = (b ∪ {y})} k) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))))
108107com23 72 . . . . . . . . . . . . . . 15 ((k Nn (c k z c)) → ((y c → {x b c x = (b ∪ {y})} k) → (y ( ∼ c ∩ ∼ {z}) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))))
10963, 108syld 40 . . . . . . . . . . . . . 14 ((k Nn (c k z c)) → (l k (y l → {x b l x = (b ∪ {y})} k) → (y ( ∼ c ∩ ∼ {z}) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))))
110109imp 418 . . . . . . . . . . . . 13 (((k Nn (c k z c)) l k (y l → {x b l x = (b ∪ {y})} k)) → (y ( ∼ c ∩ ∼ {z}) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c)))
111110an32s 779 . . . . . . . . . . . 12 (((k Nn l k (y l → {x b l x = (b ∪ {y})} k)) (c k z c)) → (y ( ∼ c ∩ ∼ {z}) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c)))
112 unieq 3900 . . . . . . . . . . . . . . . 16 (a = (c ∪ {z}) → a = (c ∪ {z}))
113112compleqd 3245 . . . . . . . . . . . . . . 15 (a = (c ∪ {z}) → ∼ a = ∼ (c ∪ {z}))
114 uniun 3910 . . . . . . . . . . . . . . . . 17 (c ∪ {z}) = (c{z})
115114compleqi 3244 . . . . . . . . . . . . . . . 16 (c ∪ {z}) = ∼ (c{z})
116 iunin 3547 . . . . . . . . . . . . . . . 16 ∼ (c{z}) = ( ∼ c ∩ ∼ {z})
117115, 116eqtri 2373 . . . . . . . . . . . . . . 15 (c ∪ {z}) = ( ∼ c ∩ ∼ {z})
118113, 117syl6eq 2401 . . . . . . . . . . . . . 14 (a = (c ∪ {z}) → ∼ a = ( ∼ c ∩ ∼ {z}))
119118eleq2d 2420 . . . . . . . . . . . . 13 (a = (c ∪ {z}) → (y ay ( ∼ c ∩ ∼ {z})))
120 rexeq 2808 . . . . . . . . . . . . . . . 16 (a = (c ∪ {z}) → (b a x = (b ∪ {y}) ↔ b (c ∪ {z})x = (b ∪ {y})))
121120abbidv 2467 . . . . . . . . . . . . . . 15 (a = (c ∪ {z}) → {x b a x = (b ∪ {y})} = {x b (c ∪ {z})x = (b ∪ {y})})
122 unab 3521 . . . . . . . . . . . . . . . 16 ({x b c x = (b ∪ {y})} ∪ {x x = (z ∪ {y})}) = {x (b c x = (b ∪ {y}) x = (z ∪ {y}))}
123 df-sn 3741 . . . . . . . . . . . . . . . . 17 {(z ∪ {y})} = {x x = (z ∪ {y})}
124123uneq2i 3415 . . . . . . . . . . . . . . . 16 ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) = ({x b c x = (b ∪ {y})} ∪ {x x = (z ∪ {y})})
125 rexun 3443 . . . . . . . . . . . . . . . . . 18 (b (c ∪ {z})x = (b ∪ {y}) ↔ (b c x = (b ∪ {y}) b {z}x = (b ∪ {y})))
126 uneq1 3411 . . . . . . . . . . . . . . . . . . . . 21 (b = z → (b ∪ {y}) = (z ∪ {y}))
127126eqeq2d 2364 . . . . . . . . . . . . . . . . . . . 20 (b = z → (x = (b ∪ {y}) ↔ x = (z ∪ {y})))
12866, 127rexsn 3768 . . . . . . . . . . . . . . . . . . 19 (b {z}x = (b ∪ {y}) ↔ x = (z ∪ {y}))
129128orbi2i 505 . . . . . . . . . . . . . . . . . 18 ((b c x = (b ∪ {y}) b {z}x = (b ∪ {y})) ↔ (b c x = (b ∪ {y}) x = (z ∪ {y})))
130125, 129bitri 240 . . . . . . . . . . . . . . . . 17 (b (c ∪ {z})x = (b ∪ {y}) ↔ (b c x = (b ∪ {y}) x = (z ∪ {y})))
131130abbii 2465 . . . . . . . . . . . . . . . 16 {x b (c ∪ {z})x = (b ∪ {y})} = {x (b c x = (b ∪ {y}) x = (z ∪ {y}))}
132122, 124, 1313eqtr4ri 2384 . . . . . . . . . . . . . . 15 {x b (c ∪ {z})x = (b ∪ {y})} = ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})})
133121, 132syl6eq 2401 . . . . . . . . . . . . . 14 (a = (c ∪ {z}) → {x b a x = (b ∪ {y})} = ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}))
134133eleq1d 2419 . . . . . . . . . . . . 13 (a = (c ∪ {z}) → ({x b a x = (b ∪ {y})} (k +c 1c) ↔ ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c)))
135119, 134imbi12d 311 . . . . . . . . . . . 12 (a = (c ∪ {z}) → ((y a → {x b a x = (b ∪ {y})} (k +c 1c)) ↔ (y ( ∼ c ∩ ∼ {z}) → ({x b c x = (b ∪ {y})} ∪ {(z ∪ {y})}) (k +c 1c))))
136111, 135syl5ibrcom 213 . . . . . . . . . . 11 (((k Nn l k (y l → {x b l x = (b ∪ {y})} k)) (c k z c)) → (a = (c ∪ {z}) → (y a → {x b a x = (b ∪ {y})} (k +c 1c))))
137136rexlimdvva 2745 . . . . . . . . . 10 ((k Nn l k (y l → {x b l x = (b ∪ {y})} k)) → (c k z ca = (c ∪ {z}) → (y a → {x b a x = (b ∪ {y})} (k +c 1c))))
13853, 137syl5bi 208 . . . . . . . . 9 ((k Nn l k (y l → {x b l x = (b ∪ {y})} k)) → (a (k +c 1c) → (y a → {x b a x = (b ∪ {y})} (k +c 1c))))
139138ralrimiv 2696 . . . . . . . 8 ((k Nn l k (y l → {x b l x = (b ∪ {y})} k)) → a (k +c 1c)(y a → {x b a x = (b ∪ {y})} (k +c 1c)))
140139ex 423 . . . . . . 7 (k Nn → (l k (y l → {x b l x = (b ∪ {y})} k) → a (k +c 1c)(y a → {x b a x = (b ∪ {y})} (k +c 1c))))
1419, 31, 34, 46, 49, 52, 140finds 4411 . . . . . 6 (N Nnl N (y l → {x b l x = (b ∪ {y})} N))
142 unieq 3900 . . . . . . . . . 10 (l = Ll = L)
143142compleqd 3245 . . . . . . . . 9 (l = L → ∼ l = ∼ L)
144143eleq2d 2420 . . . . . . . 8 (l = L → (y ly L))
145 rexeq 2808 . . . . . . . . . 10 (l = L → (b l x = (b ∪ {y}) ↔ b L x = (b ∪ {y})))
146145abbidv 2467 . . . . . . . . 9 (l = L → {x b l x = (b ∪ {y})} = {x b L x = (b ∪ {y})})
147146eleq1d 2419 . . . . . . . 8 (l = L → ({x b l x = (b ∪ {y})} N ↔ {x b L x = (b ∪ {y})} N))
148144, 147imbi12d 311 . . . . . . 7 (l = L → ((y l → {x b l x = (b ∪ {y})} N) ↔ (y L → {x b L x = (b ∪ {y})} N)))
149148rspccv 2952 . . . . . 6 (l N (y l → {x b l x = (b ∪ {y})} N) → (L N → (y L → {x b L x = (b ∪ {y})} N)))
150141, 149syl 15 . . . . 5 (N Nn → (L N → (y L → {x b L x = (b ∪ {y})} N)))
151150com3r 73 . . . 4 (y L → (N Nn → (L N → {x b L x = (b ∪ {y})} N)))
1528, 151vtoclga 2920 . . 3 (X L → (N Nn → (L N → {x b L x = (b ∪ {X})} N)))
153152com3l 75 . 2 (N Nn → (L N → (X L → {x b L x = (b ∪ {X})} N)))
1541533imp 1145 1 ((N Nn L N X L) → {x b L x = (b ∪ {X})} N)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358   w3a 934  wal 1540   = wceq 1642   wcel 1710  {cab 2339  wral 2614  wrex 2615  ccompl 3205  cun 3207  cin 3208  c0 3550  {csn 3737  cuni 3891  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-0c 4377  df-addc 4378  df-nnc 4379
This theorem is referenced by:  nnadjoinpw  4521
  Copyright terms: Public domain W3C validator